D:Dsys.
Feasible(D)
 (dec:(i,a:IdM(i).state(M(i).da(locl(a))+Unit)), i:Id.
 (d-machine(i;M(i);dec(i))
 ( w-automaton(x.M(i).ds(x);a.M(i).da(locl(a));l,tg. M(source(l)).dout(l,tg))) 

latex

Definitions

{T}, P  Q, x:A. B(x), SQType(T), Id, s = t, Prop, s ~ t, x:AB(x), M.dout(l,tg), x:AB(x), <a,b>, P & Q, P  Q, b, {x:A| B(x) }, IdLnk, x. t(x), 1of(t), Type, Msg(M), Msg(da), type List, State(ds), locl(a), M.sends(k,s,v), Feasible(D), M.da(a), Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, f(x)?z, rcv(l,tg), M.ds(x), S  T, f(a), filter(P;l), nil, M.ef(k,x,s,v)?w, destination(l), A, b, , Unit, left+right, lnk(k), islocal(k), tag(k), act(k), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, x,y. t(x;y), p  q, S  T, d-machine(i;M;dec), w-automaton(T;TA;M), Dsys, mlnk(m), source(l), a = b, x.A(x), M(i), M.Msg, M.state, t  T

Lemmas

d-feasible wf, dsys wf, ma-st wf, unit wf, bor wf, islocal wf, lnk wf, Knd wf, kindcase wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, bool wf, bnot wf, not wf, ldst wf, ma-ef-val wf, filter wf, ma-ds wf, ma-da wf, rcv wf, ma-send-val wf, locl wf, filter type, mlnk wf d, ma-msg wf, subtype rel list, assert wf, eq id wf, pi1 wf, IdLnk wf, assert-eq-id, ma-dout wf, d-m wf, lsrc wf, Id wf, Id sq